Nuprl Lemma : ma-interface-kinds-aux1
11,40
postcript
pdf
A
:Type,
I
:MaInterface(
A
). map(
i
.(
I
(
i
).2).1;
I
.1)
(Knd List List)
latex
Definitions
Type
,
t
T
,
x
:
A
.
B
(
x
)
,
MaInterface(
T
)
,
f
(
x
)
,
t
.2
,
t
.1
,
map(
f
;
as
)
,
Knd
,
type
List
,
x
:
A
B
(
x
)
,
b
,
a
:
A
fp
B
(
a
)
,
State(
ds
)
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
Atom$n
,
IdDeq
,
x
.
A
(
x
)
,
Id
,
(
x
l
)
,
{
x
:
A
|
B
(
x
)}
,
s
=
t
,
a
<
b
,
S
T
,
f
(
x
)?
z
,
x
.
t
(
x
)
,
hasloc(
k
;
i
)
,
f
(
a
)
Lemmas
list-subtype
,
Knd
wf
,
assert
wf
,
hasloc
wf
,
pi2
wf
,
pi1
wf
,
decl-state
wf
,
map
wf
,
l
member
wf
,
ma-interface
wf
origin
A:Type, I:MaInterface(A). map(
i.(I(i).2).1;I.1) 
(Knd List List) A:Type, I:MaInterface(A). map(i.(I(i).2).1;I.1) (Knd List List) Tx:A. B(x)
B(x)
b
B(a)
B(x)x.A(x) l)
T
x. t(x)